Nuprl Lemma : last-solution_wf
11,40
postcript
pdf
es
:ES,
P
:(E
),
d
:(
a
:E
Dec(
P
(
a
))). last-solution(
es
;
P
;
d
)
E
(E + Top)
latex
Definitions
suptype(
S
;
T
)
,
S
T
,
x
.
t
(
x
)
,
(
e
<loc
e'
)
,
P
&
Q
,
e
loc
e'
,
A
c
B
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
last-solution(
es
;
P
;
d
)
,
Top
,
t
T
,
x
(
s
)
,
,
x
:
A
.
B
(
x
)
Lemmas
event
system
wf
,
es-E
wf
,
top
wf
,
pi1
wf
,
es-le
wf
,
alle-le
wf
,
decidable
wf
,
not
wf
,
es-causl
wf
,
es-loc
wf
,
Id
wf
,
es-le-loc
,
es-locl
wf
origin
es:ES, P:(E
), d:(a:EDec(P(a))). last-solution(es;P;d) 
E(E + Top) es:ES, P:(E), d:(a:EDec(P(a))). last-solution(es;P;d) E(E + Top) 
T
x. t(x)
loc e' 
B
x:A. B(x)
Q
Q Tx:A. B(x)